(set-logic LIA)
(declare-const a Int)
(declare-const b Int)
(assert (< (+ a 4) b))
(assert (forall ((x Int) (y Int))
	  (=> (and (<= a (* 3 x)) (<= (* 3 x) b) 
                   (<= a (* 3 y)) (<= (* 3 y) b))
	      (= x y))))
(check-sat)
(exit)
